STM: chain sys wf

ABS: csinput(cmd)

STM: csinput wf

ABS: csupdate(from;cmds)

STM: csupdate wf

ABS: chain_sys_ind(x;cmd.input(cmd);from,cmds.update(from;cmds))

STM: chain sys ind wf

STM: chain sys-induction

ABS: chain sys ind csinput compseq tag def

ABS: chain sys ind csupdate compseq tag def

ABS: csinput?(x)

STM: csinput? wf

ABS: csinput-cmd(x)

STM: csinput-cmd wf

ABS: csupdate?(x)

STM: csupdate? wf

ABS: csupdate-from(x)

STM: csupdate-from wf

ABS: csupdate-cmds(x)

STM: csupdate-cmds wf